package at.tasat.test.level3;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.InputStreamReader;

import at.tasat.cnf.Cnf;
import at.tasat.parser.DimacsParser;
import at.tasat.solver.Solver;
import at.tasat.solver.SolverException;

public class ReferenceComparer {
	private static final String REFERENCE_EXECUTABLE = "test/reference/lingeling";

	public static void main(String[] args) {
		File file = new File(args[0]);
		try {
			boolean referenceSat = runReference(file);
			boolean implementationSat = runImplementation(file);
			int returnValue = (referenceSat == implementationSat ? 0 : 1);
			System.exit(returnValue);
		} catch (Throwable t) {
			System.err.println(t.toString());
			System.exit(2);
		}
	}

	private static boolean runReference(File file) throws IOException, InterruptedException {
		File executable = new File(REFERENCE_EXECUTABLE);
		ProcessBuilder referenceBuilder = new ProcessBuilder(executable.getAbsolutePath(), file.getAbsolutePath());
		Process process = referenceBuilder.start();
		process.waitFor();
		String result = new BufferedReader(new InputStreamReader(process.getInputStream())).readLine();
		if (result.contains("UNSATISFIABLE")) {
			return false;
		} else if (result.contains("SATISFIABLE")) {
			return true;
		}
		throw new RuntimeException("?");
	}

	private static boolean runImplementation(File file) throws FileNotFoundException, IOException, InterruptedException, SolverException {
		Cnf cnf = DimacsParser.parse(new FileInputStream(file));
		Solver solver = Solver.create(cnf);
		boolean result = solver.solve();
		solver.releaseThreadManager();
		return result;
	}
}
